﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Pex.Framework;
using Microsoft.Pex.Framework.Goals;

namespace MicroBenchmarks.DataStructures
{
    /// <summary>
    /// Checks common datastructure dictionary
    /// </summary>
    [PexClass]
    [PexMe.Attribute.FieldAccessObserver]
    [PexMe.Attribute.InsufficientObjectFactoryObserver]
    public partial class DictionaryTest
    {
        [PexMethod]
        [PexAssertReachEventually]
        public void DictionarySizeTest([PexAssumeUnderTest]Dictionary<string, string> dic)
        {
            if (dic.Count > 3)
                PexAssert.ReachEventually();
        }

        [PexMethod]
        [PexAssertReachEventually]
        public void DictionaryKeyTest([PexAssumeUnderTest]Dictionary<string, string> dic)
        {
            if (dic.ContainsKey("test"))
                PexAssert.ReachEventually();
        }

        [PexMethod]
        [PexAssertReachEventually]
        public void DictionaryContainsTest([PexAssumeUnderTest]Dictionary<string, string> dic)
        {
            if (dic.ContainsValue("test"))
                PexAssert.ReachEventually();
        }
    }
}
